FDL - Nuprl Definition : mon_when

Nuprl Definition : mon_when

when b. p == if b then p else e fi

clarification:

when{g} b. p == if b then p else eg fi

Up groups 1

Wellformedness Lemmas mon when wf

Definitions if b then t else f fi , e